package be.riaan.notanum;

trait Name 

trait Expr {
  def abstractOver(me: Name): Scope = Scope(letmeB(me, 0))
  
  def substitute(image: Expr, me: Name) = abstractOver(me).instantiate(image)
  
  // bind name `me' as `Bound(idx)'
  def letmeB(me: Name, idx: int): Expr

  // what is bound under index idx --> replace Bound(idx) by what
  def whatsB(what: Expr, idx: int): Expr
}

case class Free(n: Name) extends Expr {
  def letmeB(me: Name, idx: int) = if(n==me) Bound(idx) else this
  def whatsB(what: Expr, idx: int) = this
}
case class Bound(idx: int) extends Expr {
  def letmeB(me: Name, idx: int) = this
  def whatsB(what: Expr, idx: int) = if(this.idx == idx) what else this
}
case class App (fun: Expr, arg: Expr) extends Expr {
  def letmeB(me: Name, idx: int) = App(fun.letmeB(me, idx), arg.letmeB(me, idx)) 
  def whatsB(what: Expr, idx: int) = App(fun.whatsB(what, idx), arg.whatsB(what, idx))  
}

object Univ {
  def apply(b: Binding, range: Expr): Univ = Univ(b.domain, range.abstractOver(b.name))
  def apply(domain: Expr, body: Scope): Univ = new Univ(domain, body)
}
class Univ(val domain: Expr, val body: Scope) extends Expr {
  def letmeB(me: Name, idx: int) = Univ(domain.letmeB(me, idx), body.letmeB(me, idx)) 
  def whatsB(what: Expr, idx: int) = Univ(domain.whatsB(what, idx), body.whatsB(what, idx))
}

case class Scope(body: Expr) {
  def instantiate(image: Expr): Expr = body.whatsB(image, 0)
  
  def letmeB(me: Name, idx: int): Scope = Scope(body.letmeB(me, idx+1))
  def whatsB(what: Expr, idx: int): Scope = Scope(body.whatsB(what, idx+1)) 
}

case class Binding(name: Name, domain: Expr) {
  def freeVar = Free(name)
  
}